Problem: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Proof: Complexity Transformation Processor: strict: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [log](x0) = x0 + 43, [s](x0) = x0 + 21, [half](x0) = x0 + 48, [0] = 64 orientation: half(0()) = 112 >= 64 = 0() half(s(s(x))) = x + 90 >= x + 69 = s(half(x)) log(s(0())) = 128 >= 64 = 0() log(s(s(x))) = x + 85 >= x + 133 = s(log(s(half(x)))) problem: strict: log(s(s(x))) -> s(log(s(half(x)))) weak: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() Arctic Interpretation Processor: dimension: 2 interpretation: [1 -&] [log](x0) = [2 0 ]x0, [0 1] [s](x0) = [7 0]x0, [0 -&] [half](x0) = [0 -&]x0, [0 ] [0] = [-&] orientation: [9 2 ] [8 -&] log(s(s(x))) = [10 8 ]x >= [9 -&]x = s(log(s(half(x)))) [0] [0 ] half(0()) = [0] >= [-&] = 0() [8 1] [1 -&] half(s(s(x))) = [8 1]x >= [7 -&]x = s(half(x)) [1] [0 ] log(s(0())) = [7] >= [-&] = 0() problem: strict: weak: log(s(s(x))) -> s(log(s(half(x)))) half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() Qed